A:Type, B:(AType), eq:EqDecider(A), f,g:fpf(A; a.B(a)), x:A.
(fpf-dom(eq; x; fpf-join(eq; f; g)))  ((fpf-dom(eq; x; f))  (fpf-dom(eq; x; g))) 

latex

Definitions	True, (x  l), P  Q, t  T, x:A. B(x), x(s), x. t(x), prop{i:l}, P  Q, P  Q, P  Q, P  Q, False, , b, A, b, Unit, filter(P; l), append(as; bs), EqDecider(T), fpf-dom(eq; x; f), fpf-join(eq; f; g), fpf(A; a.B(a)), t.1, deq-member(eq; x; L), guard(T)
Lemmas	deq wf, member append, append wf, iff functionality wrt iff, or functionality wrt iff, member filter, filter wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, bnot wf, not wf, assert wf, deq-member wf, bool wf, false wf, true wf, pi1 wf, l member wf